Nuprl Lemma : as_strong_wf 4,23

T:Type, Q, P:(TProp). P as strong as Q   Prop 
latex


DefinitionsP as strong as Q , x:A. B(x), P  Q, Prop, t  T

origin